Inference at * 
Iof proof for Lemma linorder lt neg:


  T:Type, R:(TT).
  (x, y:T. Dec(R(x,y)))
   Linorder(T;x,y.R(x,y))
   (a, b:T. (strict_part(x,y.R(x,y);a;b))  R(b,a)) 

latex

 by ((((((RepD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term)))) 
CollapseTHEN (ARepD ["compound";"basic"]))) 
CollapseTHEN (
CUnfold `strict_part` 0)) 

latex

C1: 

C1: 1. T : Type
C1: 2. R : TT
C1: 3. x, y:T. Dec(R(x,y))
C1: 4. a:T. R(a,a)
C1: 5. a, b, c:T. R(a,b)  R(b,c)  R(a,c)
C1: 6. x, y:T. R(x,y)  R(y,x)  (x = y)
C1: 7. x, y:T. R(x,y)  R(y,x)
C1: 8. a : T
C1: 9. b : T
C1:   ((R(a,b) & (R(b,a))))  R(b,a)
C.

Definitions	x,y. t(x;y), t  T, strict_part(x,y.R(x;y);a;b), x(s1,s2), P  Q, , x:A. B(x), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), P & Q, Linorder(T;x,y.R(x;y))
Lemmas	decidable wf, linorder wf